/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transl;

import java.io.PrintStream;
import java.util.Map;

import alloy.ast.Formula;
import alloy.ast.LeafExpr;
import alloy.ast.LeafId;
import alloy.ast.Node;
import alloy.type.RelationType;

/**
 * A read-only interface for getting the {@linkplain Transl Boolean translation} of any {@linkplain Node AST node}.
 * You can use this translation to find the value to which the node evaluates under a particular Alloy instance.
 * See methods {@link #getNodeTransl} and {@link #getLeafTransl}.
 *
 * <p>
 * Since this interface extends {@link ASTInfo} it also inherits methods that return various information
 * about the Alloy formula that was translated, for example the list of all relations.
 */
public interface TranslInfo extends ASTInfo {
    /** @return the {@link BoolVarAllocator} used to allocate boolean variables during translation.
	After translation, it can be queried for some useful information such as how many boolean
	variables were allocated to relations referenced in the {@link Formula}. */
    public BoolVarAllocator getBoolVarAllocator();

    /**
     * Return the object that assigned Boolean variables to relations.
     */
    public RelationAllocator getRelationAllocator();

    /** @return {@link Map} from {@link LeafExpr} corresponding to each relation
        to its {@link ExprTransl}.  Used in constructing {@link alloy.gui.SolutionData}
        implementations. */
    public Map /* LeafExpr->ExprTransl */ getRelationExprsToTransls();

    /**
     * Return the Boolean {@linkplain Transl translation} for {@linkplain alloy.ast.Leaf leaf nodes} with
     * the given {@link LeafId} (they all have the same Boolean translation since they all represent the same
     * entity, e.g. the same relation or the same quantified variable or the same integer constant).
     */
    public Transl getLeafTransl(LeafId leafId_);

//     /** @return the {@link BoolSwitch} allocated to the quantified {@link Variable}
// 	with the given {@link LeafId}. */
//     public BoolSwitch getVarSwitch(LeafId varLeafId_);

    /**
     * Return a {@link QVarIterationInfo} object that describes the values through which
     * the given quantified variable runs.
     */
    public QVarIterationInfo getQVarIterationInfo(LeafId qvarLeafId_);
	
    /**
     * Returns the {@link Transl}ation of a given AST node.  The translation contains one or more
     * Boolean formulas representing the value of the node in terms of the values of Boolean variables
     * {@linkplain RelationAllocator allocated} to the relations.
     * For a {@linkplain alloy.ast.Formula Boolean-valued node} this returns a {@link FormulaTransl},
     * for a {@linkplain alloy.ast.Expr relation-valued node} this returns an {@link ExprTransl},
     * for an {@linkplain alloy.ast.IntExpr integer-valued node} this return an {@link IntTransl}.
     */
    public Transl getNodeTransl(Node node_);

    /** @return {@link Map} from {@link ExprTransl} translation of each relation
	to its {@link RelationType}.  Used by {@link alloy.symm.SymmetryBreaker} to
	construct a symmetry-breaking predicate. */
    public Map /* ExprTransl->RelationType */ getRelationTransls();

    /** Print out the value of each relation for the given instance.
	(We gathered a list of relations, {@link #_relations},
	during translation.) 
        Specify output stream by 2nd argument, or standard output by default. */
    public void interpretRelations(boolean[] assignment_);
    public void interpretRelations(boolean[] assignment_, PrintStream ps);
}
